n, i:. (i  upto(n))  (i < n) 

latex

Definitions	t  T, A  B, , a < b, s = t, T, {x:A| B(x)} , , upto(n), l[i], #$n, P  Q, False, A, True, Type, , x:AB(x), x:A. B(x), x:A  B(x), P & Q, i  j < k, {i..j}, |g|, S  T, A c B, Void, s ~ t, ||as||, x:A. B(x), (x  l), type List, P  Q, P  Q
Lemmas	l member wf, length wf1, upto wf, select wf, length upto, int seg wf, member wf, nat wf, select upto, le wf